package kodkod.analysis.ordering;

import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;

import kodkod.analysis.Analyzer;
import kodkod.analysis.OrderableSolver;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class StackedPromotion extends AbstractOrdering {

	Analyzer analyzer = null;
	double weight1 = 1.0;
	double weight2 = 2.0;
	
	public StackedPromotion(Analyzer analyzer, double weight1, double weight2) {
		super();
		this.analyzer = analyzer;
		this.weight1 = weight1;
		this.weight2 = weight2;
	}
	
	public void apply(Translation translation) {
		if (analyzer == null) {
			analyzer = new Analyzer(translation);
		}
		int index = analyzer.getRelationIdsOrdered().get(0);
		
		for (int pos = 0, n = translation.primaryRelations.size(); pos < n; pos++) {
			Relation rel = translation.primaryRelations.get(pos);
			int[] vars = translation.primaryVariables(rel).toArray();
			double weight = pos == index ? weight2 : weight1;
			for (int var : vars) {
				weightVariable((OrderableSolver)translation.cnf(), var, weight);
			}
		}
	}
	
	public String toString() {
		StringBuffer buf = new StringBuffer();
		if (softOrder) {
			buf.append("StackedInitialize");
			DecimalFormatSymbols symbols = new DecimalFormatSymbols();
			symbols.setDecimalSeparator('.');
			NumberFormat format = new DecimalFormat("#0.00", symbols);
			buf.append("(");
			buf.append(format.format(weight1));
			buf.append(",");
			buf.append(format.format(weight2));
			buf.append(")");
		} else {
			buf.append("StackedOverride");
		}
		return buf.toString();
	}
}